;; Copyright © 2016, cage
;; All rights reserved.

;; Redistribution and use in source and binary forms, with or without
;; modification, are permitted provided that the following conditions are met:

;;     * Redistributions of source code must retain the above copyright
;; notice, this list of conditions and the following disclaimer.
;;     * Redistributions in binary form must reproduce the above copyright
;; notice, this list of conditions and the following disclaimer in the
;; documentation and/or other materials provided with the distribution.

;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
;; AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
;; LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
;; CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
;; SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
;; CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
;; ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
;; THE POSSIBILITY OF SUCH DAMAGE.

(in-package :mu-kanren)

;; just a thin wrapper just for didactical purposes
(defmacro lambda-g ((&rest parameters) &body body)
  `(lambda ,parameters ,@body))

;; see above
(defmacro lambda-$ ((&rest parameters) &body body)
  `(lambda ,parameters ,@body))

(define-constant +empty-state+ (cons nil 0)
  :test #'equalp
  :documentation "The empty state")

(define-constant +mzero+ '()
  :test #'eq
  :documentation "The empty stream")

(defparameter +failed-unification+
  (lambda-g (subst) (declare (ignore subst)) '()))

(defun failed-unification-p (s)
  (eq s +failed-unification+))

(defclass mu-var ()
  ((id
    :initform 0
    :initarg :id
    :accessor id
    :type     number)))

(defparameter *print-mu-var-reference-p* nil)

(defparameter *print-mu-var-type-p*      nil)

(defmethod print-object ((object mu-var) stream)
  (with-accessors ((id id)) object
    (print-unreadable-object (object stream
			      :type     *print-mu-var-type-p*
			      :identity *print-mu-var-reference-p*)
      (format stream "~a" id))))

(defun mu-var-p (a)
  (typep a 'mu-var))

(defun mu-var (&optional (a 0))
  (make-instance 'mu-var :id a))

(defun mu-var-id (a)
  (id a))

(defun mu-var= (a b)
  (and (mu-var-p a)
       (mu-var-p b)
       (= (mu-var-id a)
	  (mu-var-id b))))

(defun var-exists-in-subst-fn ()
  #'(lambda (a b) (mu-var= a b)))

(defun var-exists-in-subst-p (v subst)
  (assoc v subst :test (var-exists-in-subst-fn)))

(defun walk (u subst)
  (let ((pr (and (mu-var-p u)
		 (var-exists-in-subst-p u subst))))
    (if pr
	(walk (cdr pr) subst)
	u)))

(defun occurs-check (x v subst)
  (let ((v (walk v subst)))
    (cond
      ((mu-var-p v)
       (mu-var= v x))
      ((consp v)
       (or (occurs-check x (car v) subst)
	   (occurs-check x (cdr v) subst)))
      (t nil))))

(defun extend-subst (rhs lhs subst)
  (if (occurs-check rhs lhs subst)
      +failed-unification+
      (%extend-subst rhs lhs subst)))

(defun %extend-subst (x v s)
  (cons (cons x v)
	s))

(defun unit (s/c)
  (cons s/c +mzero+))

(defgeneric unify-impl (v w subst))

(defgeneric equivp (lhs rhs))

;; please note  that in  this procedure  all the  cond clauses  in the
;; original  paper   has  been  replaced  by   method  conbination  in
;; interface.lisp
(defun unify (u v subst)
  (let ((u (walk u subst))
        (v (walk v subst)))
    (unify-impl u v subst)))

(defun call/fresh (f)
  (lambda-g (s/c)
    (let ((c (cdr s/c)))
      (funcall (funcall f (mu-var c))
	       (cons (car s/c)
		     (1+ c))))))

(defun == (u v)
  (lambda-g (s/c)
    (let ((s (unify u v (car s/c))))
      (if (not (failed-unification-p s))
	  (unit (cons s (cdr s/c)))
	  +mzero+))))

(defun mplus ($1 $2)
  (cond
    ((null $1)
     $2)
    ((functionp $1)
     (lambda-$ () (mplus $2 (funcall $1))))
    (t
     (cons (car $1)
	   (mplus $2 (cdr $1))))))

(defun bind ($ g)
  (cond
    ((null $)
     +mzero+)
    ((functionp $)
     (lambda-$ () (bind (funcall $) g)))
    (t
     (mplus (funcall g (car $))
	    (bind (cdr $) g)))))

(defun disj (g1 g2)
  (lambda-g (s/c) (mplus (funcall g1 s/c)
			 (funcall g2 s/c))))

(defun conj (g1 g2)
  (lambda-g (s/c) (bind (funcall g1 s/c)
			g2)))

;; mu-kanren ends here
